Search Results

Documents authored by Schmidt-Schauß, Manfred

Document
DOI: 10.4230/LIPIcs.FSCD.2022.7
Nominal Anti-Unification with Atom-Variables

Authors: Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Anti-unification is the task of generalizing a set of expressions in the most specific way. It was extended to the nominal framework by Baumgarter, Kutsia, Levy and Villaret, who defined an algorithm solving the nominal anti-unification problem, which runs in polynomial time. Unfortunately, when an infinite set of atoms are allowed in generalizations, a minimal complete set of solutions in nominal anti-unification does not exist, in general. In this paper, we present a more general approach to nominal anti-unification that uses atom-variables instead of explicit atoms, and two variants of freshness constraints: NL_A-constraints (with atom-variables), and Eqr-constraints based on Equivalence relations on atom-variables. The idea of atom-variables is that different atom-variables may be instantiated with identical or different atoms. Albeit simple, this freedom in the formulation increases its application potential: we provide an algorithm that is finitary for the NL_A-freshness constraints, and for Eqr-freshness constraints it computes a unique least general generalization. There is a price to pay in the general case: checking freshness constraints and other related logical questions will require exponential time. The setting of Baumgartner et al. is improved by the atom-only case, which runs in polynomial time and computes a unique least general generalization.
Cite as

Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho. Nominal Anti-Unification with Atom-Variables. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2022.7,
  author =	{Schmidt-Schau{\ss}, Manfred and Nantes-Sobrinho, Daniele},
  title =	{{Nominal Anti-Unification with Atom-Variables}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{7:1--7:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.7},
  URN =		{urn:nbn:de:0030-drops-162885},
  doi =		{10.4230/LIPIcs.FSCD.2022.7},
  annote =	{Keywords: Generalization, anti-unification, nominal algorithms, higher-order deduction}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.28
Nominal Unification with Atom and Context Variables

Authors: Manfred Schmidt-Schauß and David Sabel

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Automated deduction in higher-order program calculi, where properties of transformation rules are demanded, or confluence or other equational properties are requested, can often be done by syntactically computing overlaps (critical pairs) of reduction rules and transformation rules. Since higher-order calculi have alpha-equivalence as fundamental equivalence, the reasoning procedure must deal with it. We define ASD1-unification problems, which are higher-order equational unification problems employing variables for atoms, expressions and contexts, with additional distinct-variable constraints, and which have to be solved w.r.t. alpha-equivalence. Our proposal is to extend nominal unification to solve these unification problems. We succeeded in constructing the nominal unification algorithm NomUnifyASD. We show that NomUnifyASD is sound and complete for this problem class, and outputs a set of unifiers with constraints in nondeterministic polynomial time if the final constraints are satisfiable. We also show that solvability of the output constraints can be decided in NEXPTIME, and for a fixed number of context-variables in NP time. For terms without context-variables and atom-variables, NomUnifyASD runs in polynomial time, is unitary, and extends the classical problem by permitting distinct-variable constraints.
Cite as

Manfred Schmidt-Schauß and David Sabel. Nominal Unification with Atom and Context Variables. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.FSCD.2018.28,
  author =	{Schmidt-Schau{\ss}, Manfred and Sabel, David},
  title =	{{Nominal Unification with Atom and Context Variables}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.28},
  URN =		{urn:nbn:de:0030-drops-91983},
  doi =		{10.4230/LIPIcs.FSCD.2018.28},
  annote =	{Keywords: automated deduction, nominal unification, lambda calculus, functional programming}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.405
Two-Restricted One Context Unification is in Polynomial Time

Authors: Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.
Cite as

Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari. Two-Restricted One Context Unification is in Polynomial Time. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 405-422, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gascon_et_al:LIPIcs.CSL.2015.405,
  author =	{Gasc\'{o}n, Adri\`{a} and Schmidt-Schau{\ss}, Manfred and Tiwari, Ashish},
  title =	{{Two-Restricted One Context Unification is in Polynomial Time}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{405--422},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.405},
  URN =		{urn:nbn:de:0030-drops-54289},
  doi =		{10.4230/LIPIcs.CSL.2015.405},
  annote =	{Keywords: context unification, first-order unification, deduction, type checking}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.WPTE.2015
OASIcs, Volume 46, WPTE'15, Complete Volume

Authors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
OASIcs, Volume 46, WPTE'15, Complete Volume
Cite as

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{chiba_et_al:OASIcs.WPTE.2015,
  title =	{{OASIcs, Volume 46, WPTE'15, Complete Volume}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015},
  URN =		{urn:nbn:de:0030-drops-52644},
  doi =		{10.4230/OASIcs.WPTE.2015},
  annote =	{Keywords: Conference proceedings, Concurrent Programming, Formal Definitions and Theory, Specifying and Verifying and Reasoning about Programs, Semantics of Programming Languages, Mathematical Logic, Grammars and Other Rewriting Systems, Deduction and Theorem Proving}
}
Document
Front Matter
DOI: 10.4230/OASIcs.WPTE.2015.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. i-xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{chiba_et_al:OASIcs.WPTE.2015.i,
  author =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{i--xvi},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.i},
  URN =		{urn:nbn:de:0030-drops-51765},
  doi =		{10.4230/OASIcs.WPTE.2015.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.31
Observing Success in the Pi-Calculus

Authors: David Sabel and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
A contextual semantics - defined in terms of successful termination and may- and should-convergence - is analyzed in the synchronous pi-calculus with replication and a constant Stop to denote success. The contextual ordering is analyzed, some nontrivial process equivalences are proved, and proof tools for showing contextual equivalences are provided. Among them are a context lemma and new notions of sound applicative similarities for may- and should-convergence. A further result is that contextual equivalence in the pi-calculus with Stop conservatively extends barbed testing equivalence in the (Stop-free) pi-calculus and thus results on contextual equivalence can be transferred to the (Stop-free) pi-calculus with barbed testing equivalence.
Cite as

David Sabel and Manfred Schmidt-Schauß. Observing Success in the Pi-Calculus. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 31-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{sabel_et_al:OASIcs.WPTE.2015.31,
  author =	{Sabel, David and Schmidt-Schau{\ss}, Manfred},
  title =	{{Observing Success in the Pi-Calculus}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{31--46},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.31},
  URN =		{urn:nbn:de:0030-drops-51808},
  doi =		{10.4230/OASIcs.WPTE.2015.31},
  annote =	{Keywords: Concurrency, Process calculi, Pi-calculus, Rewriting, Semantics}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.WPTE.2014
OASIcs, Volume 40, WPTE'14, Complete Volume

Authors: Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
OASIcs, Volume 40, WPTE'14, Complete Volume
Cite as

First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Proceedings{schmidtschau_et_al:OASIcs.WPTE.2014,
  title =	{{OASIcs, Volume 40, WPTE'14, Complete Volume}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014},
  URN =		{urn:nbn:de:0030-drops-46216},
  doi =		{10.4230/OASIcs.WPTE.2014},
  annote =	{Keywords: Conference proceedings, Formal Definitions and Theory, Translator writing systems and compiler generators, Specifying and Verifying and Reasoning about Programs, Semantics of Programming Languages, Mathematical Logic, Grammars and Other Rewriting Systems}
}
Document
Front Matter
DOI: 10.4230/OASIcs.WPTE.2014.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. i-xv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:OASIcs.WPTE.2014.i,
  author =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{i--xv},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.i},
  URN =		{urn:nbn:de:0030-drops-45814},
  doi =		{10.4230/OASIcs.WPTE.2014.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
Preliminary Report
DOI: 10.4230/OASIcs.WPTE.2014.63
Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)

Authors: Manfred Schmidt-Schauß and David Sabel

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract
This paper presents a call-by-need polymorphically typed lambda-calculus with letrec, case, constructors and seq. The typing of the calculus is modelled in a system-F style. Contextual equivalence is used as semantics of expressions. We also define a call-by-name variant without letrec. We adapt several tools and criteria for recognizing correct program transformations to polymorphic typing, in particular an inductive applicative simulation.
Cite as

Manfred Schmidt-Schauß and David Sabel. Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report). In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 63-74, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:OASIcs.WPTE.2014.63,
  author =	{Schmidt-Schau{\ss}, Manfred and Sabel, David},
  title =	{{Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{63--74},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.63},
  URN =		{urn:nbn:de:0030-drops-45839},
  doi =		{10.4230/OASIcs.WPTE.2014.63},
  annote =	{Keywords: functional programming, polymorphic typing, contextual equivalence, semantics}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.RTA.2011
LIPIcs, Volume 10, RTA'11, Complete Volume

Authors: Manfred Schmidt-Schauß

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
LIPIcs, Volume 10, RTA'11, Complete Volume
Cite as

22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{schmidtschau:LIPIcs.RTA.2011,
  title =	{{LIPIcs, Volume 10, RTA'11, Complete Volume}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011},
  URN =		{urn:nbn:de:0030-drops-41045},
  doi =		{10.4230/LIPIcs.RTA.2011},
  annote =	{Keywords: Programming Techniques, Software Engineering, Programming Languages, Computation by Abstract Devices, Analysis of Algorithms and Problem Complexity Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Symbolic and Algebraic Manipulation, Artificial Intelligence}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.239
Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings

Authors: Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.
Cite as

Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel. Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 239-254, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.RTA.2013.239,
  author =	{Schmidt-Schau{\ss}, Manfred and Machkasova, Elena and Sabel, David},
  title =	{{Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{239--254},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.239},
  URN =		{urn:nbn:de:0030-drops-40651},
  doi =		{10.4230/LIPIcs.RTA.2013.239},
  annote =	{Keywords: lazy lambda calculus, contextual semantics, conservativity}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.255
Algorithms for Extended Alpha-Equivalence and Complexity

Authors: Manfred Schmidt-Schauß, Conrad Rau, and David Sabel

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
Equality of expressions in lambda-calculi, higher-order programming languages, higher-order programming calculi and process calculi is defined as alpha-equivalence. Permutability of bindings in let-constructs and structural congruence axioms extend alpha-equivalence. We analyse these extended alpha-equivalences and show that there are calculi with polynomial time algorithms, that a multiple-binding "let" may make alpha-equivalence as hard as finding graph-isomorphisms, and that the replication operator in the pi-calculus may lead to an EXPSPACE-hard alpha-equivalence problem.
Cite as

Manfred Schmidt-Schauß, Conrad Rau, and David Sabel. Algorithms for Extended Alpha-Equivalence and Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 255-270, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{schmidtschau_et_al:LIPIcs.RTA.2013.255,
  author =	{Schmidt-Schau{\ss}, Manfred and Rau, Conrad and Sabel, David},
  title =	{{Algorithms for Extended Alpha-Equivalence and Complexity}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{255--270},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.255},
  URN =		{urn:nbn:de:0030-drops-40667},
  doi =		{10.4230/LIPIcs.RTA.2013.255},
  annote =	{Keywords: alpha-equivalence, higher-order calculi, deduction, pi-calculus}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.272
Matching of Compressed Patterns with Character-Variables

Authors: Manfred Schmidt-Schauß

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
We consider the problem of finding an instance of a string-pattern s in a given string under compression by straight line programs (SLP). The variables of the string pattern can be instantiated by single characters. This is a generalisation of the fully compressed pattern match, which is the task of finding a compressed string in another compressed string, which is known to have a polynomial time algorithm. We mainly investigate patterns s that are linear in the variables, i.e. variables occur at most once in s, also known as partial words. We show that fully compressed pattern matching with linear patterns can be performed in polynomial time. A polynomial-sized representation of all matches and all substitutions is also computed. Also, a related algorithm is given that computes all periods of a compressed linear pattern in polynomial time. A technical key result on the structure of partial words shows that an overlap of h+2 copies of a partial word w with at most h holes implies that w is strongly periodic.
Cite as

Manfred Schmidt-Schauß. Matching of Compressed Patterns with Character-Variables. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 272-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{schmidtschau:LIPIcs.RTA.2012.272,
  author =	{Schmidt-Schau{\ss}, Manfred},
  title =	{{Matching of Compressed Patterns with Character-Variables}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{272--287},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.272},
  URN =		{urn:nbn:de:0030-drops-34981},
  doi =		{10.4230/LIPIcs.RTA.2012.272},
  annote =	{Keywords: matching, grammar-based compression, partial words}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.RTA.2011.i
Frontmatter, Table of Contents, Preface, Conference Organization

Authors: Manfred Schmidt-Schauss

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
Frontmatter, Table of Contents, Preface, Conference Organization
Cite as

22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. i-xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{schmidtschauss:LIPIcs.RTA.2011.i,
  author =	{Schmidt-Schauss, Manfred},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{i--xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.i},
  URN =		{urn:nbn:de:0030-drops-31099},
  doi =		{10.4230/LIPIcs.RTA.2011.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.295
Simulation in the Call-by-Need Lambda-Calculus with letrec

Authors: Manfred Schmidt-Schauss, David Sabel, and Elena Machkasova

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models. We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen.
Cite as

Manfred Schmidt-Schauss, David Sabel, and Elena Machkasova. Simulation in the Call-by-Need Lambda-Calculus with letrec. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 295-310, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{schmidtschauss_et_al:LIPIcs.RTA.2010.295,
  author =	{Schmidt-Schauss, Manfred and Sabel, David and Machkasova, Elena},
  title =	{{Simulation in the Call-by-Need Lambda-Calculus with letrec}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{295--310},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.295},
  URN =		{urn:nbn:de:0030-drops-26593},
  doi =		{10.4230/LIPIcs.RTA.2010.295},
  annote =	{Keywords: Lambda calculus, semantics, contextual equivalence, bisimulation,call-by-need}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact